;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "Imerge-sort.lisp")
(require "Mmerge-sort.lisp")

(module Tmerge-sort
  (import Imerge-sort)
  (import Imerge-sort-private)
  
  (include-book "testing" :dir :teachpacks)
    
  (include-book "doublecheck" :dir :teachpacks)
  
  (defrandom random-x ()
    (random-case
     nil :weight 0
    (list (random-list-of (string-downcase (random-string)))
          (random-integer))))
  
  (defproperty merge-sort-permutation-of-input-tst :repeat 100
    (x :value (list (random-list-of (string-downcase (random-string)))
                    (random-integer))
       :where (consp x)
     xs :value (random-list-of x)
        :where (consp xs))
    (equal (is-permutation (strip-cars (strip-cdrs (merge-sort xs))) (strip-cars (strip-cdrs xs)))
           t))
  
  (defproperty merge-sort-tst :repeat 100
    (xs :value (random-list-of (random-x))
        :where (consp (cdr xs)))
    (equal (in-increasing-order (strip-cars (strip-cdrs (merge-sort xs))))
           t))
)


(link RTmerge-sort (Mmerge-sort-private Tmerge-sort))
(invoke RTmerge-sort)